Nuprl Lemma : bor_tt_simp 13,42
u:. (u tt) = tt   
latex

Upbool 1, bool 1
Definitionst  T
Lemmasbool wf, btrue wf

origin